0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 86 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 105 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 3 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPOrderProof (⇔, 108 ms)
↳27 QDP
↳28 PisEmptyProof (⇔, 0 ms)
↳29 YES
SLOWSORTE_IN_GA(.(X1, .(X2, [])), .(X3, .(X4, []))) → U7_GA(X1, X2, X3, X4, deleteB_in_agga(X3, X1, X2, X5))
SLOWSORTE_IN_GA(.(X1, .(X2, [])), .(X3, .(X4, []))) → DELETEB_IN_AGGA(X3, X1, X2, X5)
DELETEB_IN_AGGA(X1, X2, X3, X4) → U2_AGGA(X1, X2, X3, X4, deleteA_in_aga(X1, X3, X4))
DELETEB_IN_AGGA(X1, X2, X3, X4) → DELETEA_IN_AGA(X1, X3, X4)
DELETEA_IN_AGA(X1, .(X2, X3), X4) → U1_AGA(X1, X2, X3, X4, deleteA_in_aga(X1, X3, X4))
DELETEA_IN_AGA(X1, .(X2, X3), X4) → DELETEA_IN_AGA(X1, X3, X4)
SLOWSORTE_IN_GA(.(X1, .(X2, [])), .(X3, .(X4, []))) → U8_GA(X1, X2, X3, X4, deletecB_in_agga(X3, X1, X2, X5))
U8_GA(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → U9_GA(X1, X2, X3, X4, permC_in_ga(X5, X4))
U8_GA(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → PERMC_IN_GA(X5, X4)
PERMC_IN_GA(.(X1, .(X2, [])), .(X3, .(X4, []))) → U3_GA(X1, X2, X3, X4, deleteB_in_agga(X3, X1, X2, X5))
PERMC_IN_GA(.(X1, .(X2, [])), .(X3, .(X4, []))) → DELETEB_IN_AGGA(X3, X1, X2, X5)
PERMC_IN_GA(.(X1, .(X2, [])), .(X3, .(X4, []))) → U4_GA(X1, X2, X3, X4, deletecB_in_agga(X3, X1, X2, X5))
U4_GA(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → U5_GA(X1, X2, X3, X4, permC_in_ga(X5, X4))
U4_GA(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → PERMC_IN_GA(X5, X4)
U8_GA(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → U10_GA(X1, X2, X3, X4, permcC_in_ga(X5, X4))
U10_GA(X1, X2, X3, X4, permcC_out_ga(X5, X4)) → U11_GA(X1, X2, X3, X4, leD_in_gg(X3, X4))
U10_GA(X1, X2, X3, X4, permcC_out_ga(X5, X4)) → LED_IN_GG(X3, X4)
LED_IN_GG(s(X1), s(X2)) → U6_GG(X1, X2, leD_in_gg(X1, X2))
LED_IN_GG(s(X1), s(X2)) → LED_IN_GG(X1, X2)
deletecB_in_agga(X1, X1, X2, X2) → deletecB_out_agga(X1, X1, X2, X2)
deletecB_in_agga(X1, X2, X3, X4) → U14_agga(X1, X2, X3, X4, deletecA_in_aga(X1, X3, X4))
deletecA_in_aga(X1, .(X1, X2), X2) → deletecA_out_aga(X1, .(X1, X2), X2)
deletecA_in_aga(X1, .(X2, X3), X4) → U13_aga(X1, X2, X3, X4, deletecA_in_aga(X1, X3, X4))
U13_aga(X1, X2, X3, X4, deletecA_out_aga(X1, X3, X4)) → deletecA_out_aga(X1, .(X2, X3), X4)
U14_agga(X1, X2, X3, X4, deletecA_out_aga(X1, X3, X4)) → deletecB_out_agga(X1, X2, X3, X4)
permcC_in_ga([], []) → permcC_out_ga([], [])
permcC_in_ga(.(X1, .(X2, [])), .(X3, .(X4, []))) → U15_ga(X1, X2, X3, X4, deletecB_in_agga(X3, X1, X2, X5))
U15_ga(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → U16_ga(X1, X2, X3, X4, permcC_in_ga(X5, X4))
U16_ga(X1, X2, X3, X4, permcC_out_ga(X5, X4)) → permcC_out_ga(.(X1, .(X2, [])), .(X3, .(X4, [])))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
SLOWSORTE_IN_GA(.(X1, .(X2, [])), .(X3, .(X4, []))) → U7_GA(X1, X2, X3, X4, deleteB_in_agga(X3, X1, X2, X5))
SLOWSORTE_IN_GA(.(X1, .(X2, [])), .(X3, .(X4, []))) → DELETEB_IN_AGGA(X3, X1, X2, X5)
DELETEB_IN_AGGA(X1, X2, X3, X4) → U2_AGGA(X1, X2, X3, X4, deleteA_in_aga(X1, X3, X4))
DELETEB_IN_AGGA(X1, X2, X3, X4) → DELETEA_IN_AGA(X1, X3, X4)
DELETEA_IN_AGA(X1, .(X2, X3), X4) → U1_AGA(X1, X2, X3, X4, deleteA_in_aga(X1, X3, X4))
DELETEA_IN_AGA(X1, .(X2, X3), X4) → DELETEA_IN_AGA(X1, X3, X4)
SLOWSORTE_IN_GA(.(X1, .(X2, [])), .(X3, .(X4, []))) → U8_GA(X1, X2, X3, X4, deletecB_in_agga(X3, X1, X2, X5))
U8_GA(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → U9_GA(X1, X2, X3, X4, permC_in_ga(X5, X4))
U8_GA(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → PERMC_IN_GA(X5, X4)
PERMC_IN_GA(.(X1, .(X2, [])), .(X3, .(X4, []))) → U3_GA(X1, X2, X3, X4, deleteB_in_agga(X3, X1, X2, X5))
PERMC_IN_GA(.(X1, .(X2, [])), .(X3, .(X4, []))) → DELETEB_IN_AGGA(X3, X1, X2, X5)
PERMC_IN_GA(.(X1, .(X2, [])), .(X3, .(X4, []))) → U4_GA(X1, X2, X3, X4, deletecB_in_agga(X3, X1, X2, X5))
U4_GA(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → U5_GA(X1, X2, X3, X4, permC_in_ga(X5, X4))
U4_GA(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → PERMC_IN_GA(X5, X4)
U8_GA(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → U10_GA(X1, X2, X3, X4, permcC_in_ga(X5, X4))
U10_GA(X1, X2, X3, X4, permcC_out_ga(X5, X4)) → U11_GA(X1, X2, X3, X4, leD_in_gg(X3, X4))
U10_GA(X1, X2, X3, X4, permcC_out_ga(X5, X4)) → LED_IN_GG(X3, X4)
LED_IN_GG(s(X1), s(X2)) → U6_GG(X1, X2, leD_in_gg(X1, X2))
LED_IN_GG(s(X1), s(X2)) → LED_IN_GG(X1, X2)
deletecB_in_agga(X1, X1, X2, X2) → deletecB_out_agga(X1, X1, X2, X2)
deletecB_in_agga(X1, X2, X3, X4) → U14_agga(X1, X2, X3, X4, deletecA_in_aga(X1, X3, X4))
deletecA_in_aga(X1, .(X1, X2), X2) → deletecA_out_aga(X1, .(X1, X2), X2)
deletecA_in_aga(X1, .(X2, X3), X4) → U13_aga(X1, X2, X3, X4, deletecA_in_aga(X1, X3, X4))
U13_aga(X1, X2, X3, X4, deletecA_out_aga(X1, X3, X4)) → deletecA_out_aga(X1, .(X2, X3), X4)
U14_agga(X1, X2, X3, X4, deletecA_out_aga(X1, X3, X4)) → deletecB_out_agga(X1, X2, X3, X4)
permcC_in_ga([], []) → permcC_out_ga([], [])
permcC_in_ga(.(X1, .(X2, [])), .(X3, .(X4, []))) → U15_ga(X1, X2, X3, X4, deletecB_in_agga(X3, X1, X2, X5))
U15_ga(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → U16_ga(X1, X2, X3, X4, permcC_in_ga(X5, X4))
U16_ga(X1, X2, X3, X4, permcC_out_ga(X5, X4)) → permcC_out_ga(.(X1, .(X2, [])), .(X3, .(X4, [])))
LED_IN_GG(s(X1), s(X2)) → LED_IN_GG(X1, X2)
deletecB_in_agga(X1, X1, X2, X2) → deletecB_out_agga(X1, X1, X2, X2)
deletecB_in_agga(X1, X2, X3, X4) → U14_agga(X1, X2, X3, X4, deletecA_in_aga(X1, X3, X4))
deletecA_in_aga(X1, .(X1, X2), X2) → deletecA_out_aga(X1, .(X1, X2), X2)
deletecA_in_aga(X1, .(X2, X3), X4) → U13_aga(X1, X2, X3, X4, deletecA_in_aga(X1, X3, X4))
U13_aga(X1, X2, X3, X4, deletecA_out_aga(X1, X3, X4)) → deletecA_out_aga(X1, .(X2, X3), X4)
U14_agga(X1, X2, X3, X4, deletecA_out_aga(X1, X3, X4)) → deletecB_out_agga(X1, X2, X3, X4)
permcC_in_ga([], []) → permcC_out_ga([], [])
permcC_in_ga(.(X1, .(X2, [])), .(X3, .(X4, []))) → U15_ga(X1, X2, X3, X4, deletecB_in_agga(X3, X1, X2, X5))
U15_ga(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → U16_ga(X1, X2, X3, X4, permcC_in_ga(X5, X4))
U16_ga(X1, X2, X3, X4, permcC_out_ga(X5, X4)) → permcC_out_ga(.(X1, .(X2, [])), .(X3, .(X4, [])))
LED_IN_GG(s(X1), s(X2)) → LED_IN_GG(X1, X2)
LED_IN_GG(s(X1), s(X2)) → LED_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
DELETEA_IN_AGA(X1, .(X2, X3), X4) → DELETEA_IN_AGA(X1, X3, X4)
deletecB_in_agga(X1, X1, X2, X2) → deletecB_out_agga(X1, X1, X2, X2)
deletecB_in_agga(X1, X2, X3, X4) → U14_agga(X1, X2, X3, X4, deletecA_in_aga(X1, X3, X4))
deletecA_in_aga(X1, .(X1, X2), X2) → deletecA_out_aga(X1, .(X1, X2), X2)
deletecA_in_aga(X1, .(X2, X3), X4) → U13_aga(X1, X2, X3, X4, deletecA_in_aga(X1, X3, X4))
U13_aga(X1, X2, X3, X4, deletecA_out_aga(X1, X3, X4)) → deletecA_out_aga(X1, .(X2, X3), X4)
U14_agga(X1, X2, X3, X4, deletecA_out_aga(X1, X3, X4)) → deletecB_out_agga(X1, X2, X3, X4)
permcC_in_ga([], []) → permcC_out_ga([], [])
permcC_in_ga(.(X1, .(X2, [])), .(X3, .(X4, []))) → U15_ga(X1, X2, X3, X4, deletecB_in_agga(X3, X1, X2, X5))
U15_ga(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → U16_ga(X1, X2, X3, X4, permcC_in_ga(X5, X4))
U16_ga(X1, X2, X3, X4, permcC_out_ga(X5, X4)) → permcC_out_ga(.(X1, .(X2, [])), .(X3, .(X4, [])))
DELETEA_IN_AGA(X1, .(X2, X3), X4) → DELETEA_IN_AGA(X1, X3, X4)
DELETEA_IN_AGA(.(X2, X3)) → DELETEA_IN_AGA(X3)
From the DPs we obtained the following set of size-change graphs:
PERMC_IN_GA(.(X1, .(X2, [])), .(X3, .(X4, []))) → U4_GA(X1, X2, X3, X4, deletecB_in_agga(X3, X1, X2, X5))
U4_GA(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → PERMC_IN_GA(X5, X4)
deletecB_in_agga(X1, X1, X2, X2) → deletecB_out_agga(X1, X1, X2, X2)
deletecB_in_agga(X1, X2, X3, X4) → U14_agga(X1, X2, X3, X4, deletecA_in_aga(X1, X3, X4))
deletecA_in_aga(X1, .(X1, X2), X2) → deletecA_out_aga(X1, .(X1, X2), X2)
deletecA_in_aga(X1, .(X2, X3), X4) → U13_aga(X1, X2, X3, X4, deletecA_in_aga(X1, X3, X4))
U13_aga(X1, X2, X3, X4, deletecA_out_aga(X1, X3, X4)) → deletecA_out_aga(X1, .(X2, X3), X4)
U14_agga(X1, X2, X3, X4, deletecA_out_aga(X1, X3, X4)) → deletecB_out_agga(X1, X2, X3, X4)
permcC_in_ga([], []) → permcC_out_ga([], [])
permcC_in_ga(.(X1, .(X2, [])), .(X3, .(X4, []))) → U15_ga(X1, X2, X3, X4, deletecB_in_agga(X3, X1, X2, X5))
U15_ga(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → U16_ga(X1, X2, X3, X4, permcC_in_ga(X5, X4))
U16_ga(X1, X2, X3, X4, permcC_out_ga(X5, X4)) → permcC_out_ga(.(X1, .(X2, [])), .(X3, .(X4, [])))
PERMC_IN_GA(.(X1, .(X2, [])), .(X3, .(X4, []))) → U4_GA(X1, X2, X3, X4, deletecB_in_agga(X3, X1, X2, X5))
U4_GA(X1, X2, X3, X4, deletecB_out_agga(X3, X1, X2, X5)) → PERMC_IN_GA(X5, X4)
deletecB_in_agga(X1, X1, X2, X2) → deletecB_out_agga(X1, X1, X2, X2)
deletecB_in_agga(X1, X2, X3, X4) → U14_agga(X1, X2, X3, X4, deletecA_in_aga(X1, X3, X4))
U14_agga(X1, X2, X3, X4, deletecA_out_aga(X1, X3, X4)) → deletecB_out_agga(X1, X2, X3, X4)
deletecA_in_aga(X1, .(X1, X2), X2) → deletecA_out_aga(X1, .(X1, X2), X2)
deletecA_in_aga(X1, .(X2, X3), X4) → U13_aga(X1, X2, X3, X4, deletecA_in_aga(X1, X3, X4))
U13_aga(X1, X2, X3, X4, deletecA_out_aga(X1, X3, X4)) → deletecA_out_aga(X1, .(X2, X3), X4)
PERMC_IN_GA(.(X1, .(X2, []))) → U4_GA(X1, X2, deletecB_in_agga(X1, X2))
U4_GA(X1, X2, deletecB_out_agga(X3, X1, X2, X5)) → PERMC_IN_GA(X5)
deletecB_in_agga(X1, X2) → deletecB_out_agga(X1, X1, X2, X2)
deletecB_in_agga(X2, X3) → U14_agga(X2, X3, deletecA_in_aga(X3))
U14_agga(X2, X3, deletecA_out_aga(X1, X3, X4)) → deletecB_out_agga(X1, X2, X3, X4)
deletecA_in_aga(.(X1, X2)) → deletecA_out_aga(X1, .(X1, X2), X2)
deletecA_in_aga(.(X2, X3)) → U13_aga(X2, X3, deletecA_in_aga(X3))
U13_aga(X2, X3, deletecA_out_aga(X1, X3, X4)) → deletecA_out_aga(X1, .(X2, X3), X4)
deletecB_in_agga(x0, x1)
U14_agga(x0, x1, x2)
deletecA_in_aga(x0)
U13_aga(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PERMC_IN_GA(.(X1, .(X2, []))) → U4_GA(X1, X2, deletecB_in_agga(X1, X2))
U4_GA(X1, X2, deletecB_out_agga(X3, X1, X2, X5)) → PERMC_IN_GA(X5)
POL( U4_GA(x1, ..., x3) ) = x3
POL( deletecB_in_agga(x1, x2) ) = x1 + x2 + 2
POL( deletecB_out_agga(x1, ..., x4) ) = x4 + 2
POL( U14_agga(x1, ..., x3) ) = x3 + 2
POL( deletecA_in_aga(x1) ) = x1
POL( .(x1, x2) ) = x1 + x2 + 2
POL( deletecA_out_aga(x1, ..., x3) ) = x1 + x3 + 1
POL( U13_aga(x1, ..., x3) ) = x3 + 2
POL( PERMC_IN_GA(x1) ) = x1 + 1
POL( [] ) = 0
deletecB_in_agga(X1, X2) → deletecB_out_agga(X1, X1, X2, X2)
deletecB_in_agga(X2, X3) → U14_agga(X2, X3, deletecA_in_aga(X3))
deletecA_in_aga(.(X1, X2)) → deletecA_out_aga(X1, .(X1, X2), X2)
deletecA_in_aga(.(X2, X3)) → U13_aga(X2, X3, deletecA_in_aga(X3))
U14_agga(X2, X3, deletecA_out_aga(X1, X3, X4)) → deletecB_out_agga(X1, X2, X3, X4)
U13_aga(X2, X3, deletecA_out_aga(X1, X3, X4)) → deletecA_out_aga(X1, .(X2, X3), X4)
deletecB_in_agga(X1, X2) → deletecB_out_agga(X1, X1, X2, X2)
deletecB_in_agga(X2, X3) → U14_agga(X2, X3, deletecA_in_aga(X3))
U14_agga(X2, X3, deletecA_out_aga(X1, X3, X4)) → deletecB_out_agga(X1, X2, X3, X4)
deletecA_in_aga(.(X1, X2)) → deletecA_out_aga(X1, .(X1, X2), X2)
deletecA_in_aga(.(X2, X3)) → U13_aga(X2, X3, deletecA_in_aga(X3))
U13_aga(X2, X3, deletecA_out_aga(X1, X3, X4)) → deletecA_out_aga(X1, .(X2, X3), X4)
deletecB_in_agga(x0, x1)
U14_agga(x0, x1, x2)
deletecA_in_aga(x0)
U13_aga(x0, x1, x2)